The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(1(1(2(x1)))) → 1(0(1(3(2(x1)))))
0(1(1(2(x1)))) → 4(1(0(1(2(x1)))))
0(1(1(2(x1)))) → 0(1(4(1(3(2(x1))))))
0(1(1(2(x1)))) → 0(4(1(4(1(2(x1))))))
0(1(1(2(x1)))) → 4(1(0(3(1(2(x1))))))
0(1(1(2(x1)))) → 4(1(3(1(0(2(x1))))))
0(1(1(5(x1)))) → 4(1(0(1(5(x1)))))
0(1(1(5(x1)))) → 5(4(1(0(1(x1)))))
0(1(1(5(x1)))) → 0(4(1(0(1(5(x1))))))
0(1(1(5(x1)))) → 0(5(4(1(0(1(x1))))))
0(1(1(5(x1)))) → 1(0(1(3(1(5(x1))))))
0(1(1(5(x1)))) → 1(4(4(0(1(5(x1))))))
0(1(1(5(x1)))) → 3(0(1(5(4(1(x1))))))
0(1(1(5(x1)))) → 3(4(1(0(1(5(x1))))))
0(1(1(5(x1)))) → 3(4(1(5(0(1(x1))))))
0(1(1(5(x1)))) → 3(5(4(1(0(1(x1))))))
0(1(1(5(x1)))) → 4(1(0(1(5(3(x1))))))
0(1(1(5(x1)))) → 4(1(0(1(5(4(x1))))))
0(1(1(5(x1)))) → 4(1(3(1(0(5(x1))))))
0(1(1(5(x1)))) → 4(1(4(1(0(5(x1))))))
0(1(1(5(x1)))) → 4(4(1(5(0(1(x1))))))
0(1(1(5(x1)))) → 5(4(1(3(1(0(x1))))))
0(1(2(0(x1)))) → 0(2(4(1(0(3(x1))))))
0(1(3(5(x1)))) → 0(3(5(4(1(x1)))))
0(1(4(5(x1)))) → 0(3(5(4(1(x1)))))
0(1(4(5(x1)))) → 4(4(0(1(5(3(x1))))))
0(2(4(5(x1)))) → 4(0(2(3(5(x1)))))
0(2(4(5(x1)))) → 4(4(0(2(5(x1)))))
0(2(4(5(x1)))) → 4(0(3(2(3(5(x1))))))
0(0(2(1(5(x1))))) → 0(0(2(5(4(1(x1))))))
0(0(2(4(5(x1))))) → 0(0(4(4(2(5(x1))))))
0(1(0(4(5(x1))))) → 0(4(0(0(1(5(x1))))))
0(1(0(5(0(x1))))) → 4(1(5(0(0(0(x1))))))
0(1(1(0(5(x1))))) → 1(0(4(0(1(5(x1))))))
0(1(1(2(0(x1))))) → 0(4(1(2(1(0(x1))))))
0(1(1(2(0(x1))))) → 4(1(2(1(0(0(x1))))))
0(1(1(3(5(x1))))) → 4(1(0(1(3(5(x1))))))
0(1(1(3(5(x1))))) → 5(4(1(0(3(1(x1))))))
0(1(1(4(2(x1))))) → 0(4(1(4(1(2(x1))))))
0(1(1(4(2(x1))))) → 4(1(3(1(2(0(x1))))))
0(1(1(4(2(x1))))) → 4(2(4(1(0(1(x1))))))
0(1(1(4(5(x1))))) → 0(5(4(1(3(1(x1))))))
0(1(1(4(5(x1))))) → 0(5(4(1(4(1(x1))))))
0(1(1(4(5(x1))))) → 2(4(1(0(1(5(x1))))))
0(1(2(0(2(x1))))) → 0(4(0(1(2(2(x1))))))
0(1(2(1(5(x1))))) → 0(1(4(1(2(5(x1))))))
0(1(4(5(0(x1))))) → 0(5(4(1(0(3(x1))))))
0(1(5(1(5(x1))))) → 5(4(1(0(1(5(x1))))))
0(2(0(1(5(x1))))) → 1(0(0(2(3(5(x1))))))
0(2(0(4(5(x1))))) → 0(0(2(4(1(5(x1))))))
0(2(0(5(0(x1))))) → 0(2(5(0(3(0(x1))))))
0(2(3(1(5(x1))))) → 0(0(1(2(3(5(x1))))))
0(2(3(1(5(x1))))) → 0(2(5(3(4(1(x1))))))
0(2(3(1(5(x1))))) → 0(3(5(2(4(1(x1))))))
0(2(3(1(5(x1))))) → 2(0(4(1(3(5(x1))))))
0(2(3(1(5(x1))))) → 2(0(4(1(5(3(x1))))))
0(2(3(1(5(x1))))) → 2(3(5(3(0(1(x1))))))
0(2(3(1(5(x1))))) → 2(5(3(4(1(0(x1))))))
0(2(3(1(5(x1))))) → 4(1(0(5(2(3(x1))))))
0(2(3(1(5(x1))))) → 4(1(3(0(2(5(x1))))))
0(2(3(1(5(x1))))) → 4(1(5(2(0(3(x1))))))
0(2(5(1(2(x1))))) → 0(2(3(2(1(5(x1))))))
0(2(5(1(5(x1))))) → 0(3(5(2(1(5(x1))))))
0(2(5(1(5(x1))))) → 0(4(1(5(2(5(x1))))))
0(2(5(1(5(x1))))) → 2(4(1(5(0(5(x1))))))
0(2(5(1(5(x1))))) → 4(1(0(5(2(5(x1))))))
0(2(5(1(5(x1))))) → 4(1(5(5(2(0(x1))))))
0(3(5(1(5(x1))))) → 5(0(3(5(4(1(x1))))))
0(4(2(0(2(x1))))) → 0(0(4(3(2(2(x1))))))
0(4(2(1(5(x1))))) → 0(2(5(4(4(1(x1))))))
0(4(2(1(5(x1))))) → 0(4(1(5(3(2(x1))))))
0(4(2(1(5(x1))))) → 2(4(1(0(0(5(x1))))))
0(4(2(1(5(x1))))) → 2(4(1(3(0(5(x1))))))
0(4(2(1(5(x1))))) → 2(4(1(5(4(0(x1))))))
0(4(2(1(5(x1))))) → 3(0(1(5(2(4(x1))))))
0(4(2(1(5(x1))))) → 3(0(5(2(4(1(x1))))))
0(4(2(1(5(x1))))) → 4(1(3(2(5(0(x1))))))
0(4(2(1(5(x1))))) → 4(4(0(1(5(2(x1))))))
0(4(5(1(5(x1))))) → 5(4(1(5(0(4(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c(0'(1(3(2(z0)))))
0'(1(1(2(z0)))) → c1(0'(1(2(z0))))
0'(1(1(2(z0)))) → c2(0'(1(4(1(3(2(z0)))))))
0'(1(1(2(z0)))) → c3(0'(4(1(4(1(2(z0)))))))
0'(1(1(2(z0)))) → c4(0'(3(1(2(z0)))))
0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c8(0'(4(1(0(1(5(z0)))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c10(0'(1(3(1(5(z0))))))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c12(0'(1(5(4(1(z0))))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c16(0'(1(5(3(z0)))))
0'(1(1(5(z0)))) → c17(0'(1(5(4(z0)))))
0'(1(1(5(z0)))) → c18(0'(5(z0)))
0'(1(1(5(z0)))) → c19(0'(5(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(2(0(z0)))) → c22(0'(2(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(3(5(z0)))) → c23(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c24(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c25(0'(1(5(3(z0)))))
0'(2(4(5(z0)))) → c26(0'(2(3(5(z0)))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(2(4(5(z0)))) → c28(0'(3(2(3(5(z0))))))
0'(0(2(1(5(z0))))) → c29(0'(0(2(5(4(1(z0)))))), 0'(2(5(4(1(z0))))))
0'(0(2(4(5(z0))))) → c30(0'(0(4(4(2(5(z0)))))), 0'(4(4(2(5(z0))))))
0'(1(0(4(5(z0))))) → c31(0'(4(0(0(1(5(z0)))))), 0'(0(1(5(z0)))), 0'(1(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(1(1(3(5(z0))))) → c36(0'(1(3(5(z0)))))
0'(1(1(3(5(z0))))) → c37(0'(3(1(z0))))
0'(1(1(4(2(z0))))) → c38(0'(4(1(4(1(2(z0)))))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c41(0'(5(4(1(3(1(z0)))))))
0'(1(1(4(5(z0))))) → c42(0'(5(4(1(4(1(z0)))))))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(2(0(2(z0))))) → c44(0'(4(0(1(2(2(z0)))))), 0'(1(2(2(z0)))))
0'(1(2(1(5(z0))))) → c45(0'(1(4(1(2(5(z0)))))))
0'(1(4(5(0(z0))))) → c46(0'(5(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(0(1(5(z0))))) → c48(0'(0(2(3(5(z0))))), 0'(2(3(5(z0)))))
0'(2(0(4(5(z0))))) → c49(0'(0(2(4(1(5(z0)))))), 0'(2(4(1(5(z0))))))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))
0'(2(3(1(5(z0))))) → c51(0'(0(1(2(3(5(z0)))))), 0'(1(2(3(5(z0))))))
0'(2(3(1(5(z0))))) → c52(0'(2(5(3(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c53(0'(3(5(2(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c54(0'(4(1(3(5(z0))))))
0'(2(3(1(5(z0))))) → c55(0'(4(1(5(3(z0))))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c58(0'(5(2(3(z0)))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(3(1(5(z0))))) → c60(0'(3(z0)))
0'(2(5(1(2(z0))))) → c61(0'(2(3(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c62(0'(3(5(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c63(0'(4(1(5(2(5(z0)))))))
0'(2(5(1(5(z0))))) → c64(0'(5(z0)))
0'(2(5(1(5(z0))))) → c65(0'(5(2(5(z0)))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(3(5(1(5(z0))))) → c67(0'(3(5(4(1(z0))))))
0'(4(2(0(2(z0))))) → c68(0'(0(4(3(2(2(z0)))))), 0'(4(3(2(2(z0))))))
0'(4(2(1(5(z0))))) → c69(0'(2(5(4(4(1(z0)))))))
0'(4(2(1(5(z0))))) → c70(0'(4(1(5(3(2(z0)))))))
0'(4(2(1(5(z0))))) → c71(0'(0(5(z0))), 0'(5(z0)))
0'(4(2(1(5(z0))))) → c72(0'(5(z0)))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c74(0'(1(5(2(4(z0))))))
0'(4(2(1(5(z0))))) → c75(0'(5(2(4(1(z0))))))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(2(1(5(z0))))) → c77(0'(1(5(2(z0)))))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))

S tuples:

0'(1(1(2(z0)))) → c(0'(1(3(2(z0)))))
0'(1(1(2(z0)))) → c1(0'(1(2(z0))))
0'(1(1(2(z0)))) → c2(0'(1(4(1(3(2(z0)))))))
0'(1(1(2(z0)))) → c3(0'(4(1(4(1(2(z0)))))))
0'(1(1(2(z0)))) → c4(0'(3(1(2(z0)))))
0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c8(0'(4(1(0(1(5(z0)))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c10(0'(1(3(1(5(z0))))))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c12(0'(1(5(4(1(z0))))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c16(0'(1(5(3(z0)))))
0'(1(1(5(z0)))) → c17(0'(1(5(4(z0)))))
0'(1(1(5(z0)))) → c18(0'(5(z0)))
0'(1(1(5(z0)))) → c19(0'(5(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(2(0(z0)))) → c22(0'(2(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(3(5(z0)))) → c23(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c24(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c25(0'(1(5(3(z0)))))
0'(2(4(5(z0)))) → c26(0'(2(3(5(z0)))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(2(4(5(z0)))) → c28(0'(3(2(3(5(z0))))))
0'(0(2(1(5(z0))))) → c29(0'(0(2(5(4(1(z0)))))), 0'(2(5(4(1(z0))))))
0'(0(2(4(5(z0))))) → c30(0'(0(4(4(2(5(z0)))))), 0'(4(4(2(5(z0))))))
0'(1(0(4(5(z0))))) → c31(0'(4(0(0(1(5(z0)))))), 0'(0(1(5(z0)))), 0'(1(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(1(1(3(5(z0))))) → c36(0'(1(3(5(z0)))))
0'(1(1(3(5(z0))))) → c37(0'(3(1(z0))))
0'(1(1(4(2(z0))))) → c38(0'(4(1(4(1(2(z0)))))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c41(0'(5(4(1(3(1(z0)))))))
0'(1(1(4(5(z0))))) → c42(0'(5(4(1(4(1(z0)))))))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(2(0(2(z0))))) → c44(0'(4(0(1(2(2(z0)))))), 0'(1(2(2(z0)))))
0'(1(2(1(5(z0))))) → c45(0'(1(4(1(2(5(z0)))))))
0'(1(4(5(0(z0))))) → c46(0'(5(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(0(1(5(z0))))) → c48(0'(0(2(3(5(z0))))), 0'(2(3(5(z0)))))
0'(2(0(4(5(z0))))) → c49(0'(0(2(4(1(5(z0)))))), 0'(2(4(1(5(z0))))))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))
0'(2(3(1(5(z0))))) → c51(0'(0(1(2(3(5(z0)))))), 0'(1(2(3(5(z0))))))
0'(2(3(1(5(z0))))) → c52(0'(2(5(3(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c53(0'(3(5(2(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c54(0'(4(1(3(5(z0))))))
0'(2(3(1(5(z0))))) → c55(0'(4(1(5(3(z0))))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c58(0'(5(2(3(z0)))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(3(1(5(z0))))) → c60(0'(3(z0)))
0'(2(5(1(2(z0))))) → c61(0'(2(3(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c62(0'(3(5(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c63(0'(4(1(5(2(5(z0)))))))
0'(2(5(1(5(z0))))) → c64(0'(5(z0)))
0'(2(5(1(5(z0))))) → c65(0'(5(2(5(z0)))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(3(5(1(5(z0))))) → c67(0'(3(5(4(1(z0))))))
0'(4(2(0(2(z0))))) → c68(0'(0(4(3(2(2(z0)))))), 0'(4(3(2(2(z0))))))
0'(4(2(1(5(z0))))) → c69(0'(2(5(4(4(1(z0)))))))
0'(4(2(1(5(z0))))) → c70(0'(4(1(5(3(2(z0)))))))
0'(4(2(1(5(z0))))) → c71(0'(0(5(z0))), 0'(5(z0)))
0'(4(2(1(5(z0))))) → c72(0'(5(z0)))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c74(0'(1(5(2(4(z0))))))
0'(4(2(1(5(z0))))) → c75(0'(5(2(4(1(z0))))))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(2(1(5(z0))))) → c77(0'(1(5(2(z0)))))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71, c72, c73, c74, c75, c76, c77, c78

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

0'(0(2(4(5(z0))))) → c30(0'(0(4(4(2(5(z0)))))), 0'(4(4(2(5(z0))))))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c(0'(1(3(2(z0)))))
0'(1(1(2(z0)))) → c1(0'(1(2(z0))))
0'(1(1(2(z0)))) → c2(0'(1(4(1(3(2(z0)))))))
0'(1(1(2(z0)))) → c3(0'(4(1(4(1(2(z0)))))))
0'(1(1(2(z0)))) → c4(0'(3(1(2(z0)))))
0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c8(0'(4(1(0(1(5(z0)))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c10(0'(1(3(1(5(z0))))))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c12(0'(1(5(4(1(z0))))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c16(0'(1(5(3(z0)))))
0'(1(1(5(z0)))) → c17(0'(1(5(4(z0)))))
0'(1(1(5(z0)))) → c18(0'(5(z0)))
0'(1(1(5(z0)))) → c19(0'(5(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(3(5(z0)))) → c23(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c24(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c25(0'(1(5(3(z0)))))
0'(2(4(5(z0)))) → c26(0'(2(3(5(z0)))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(2(4(5(z0)))) → c28(0'(3(2(3(5(z0))))))
0'(1(1(3(5(z0))))) → c36(0'(1(3(5(z0)))))
0'(1(1(3(5(z0))))) → c37(0'(3(1(z0))))
0'(1(1(4(2(z0))))) → c38(0'(4(1(4(1(2(z0)))))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c41(0'(5(4(1(3(1(z0)))))))
0'(1(1(4(5(z0))))) → c42(0'(5(4(1(4(1(z0)))))))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(2(1(5(z0))))) → c45(0'(1(4(1(2(5(z0)))))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c51(0'(0(1(2(3(5(z0)))))), 0'(1(2(3(5(z0))))))
0'(2(3(1(5(z0))))) → c52(0'(2(5(3(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c53(0'(3(5(2(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c54(0'(4(1(3(5(z0))))))
0'(2(3(1(5(z0))))) → c55(0'(4(1(5(3(z0))))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c58(0'(5(2(3(z0)))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(3(1(5(z0))))) → c60(0'(3(z0)))
0'(2(5(1(2(z0))))) → c61(0'(2(3(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c62(0'(3(5(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c63(0'(4(1(5(2(5(z0)))))))
0'(2(5(1(5(z0))))) → c64(0'(5(z0)))
0'(2(5(1(5(z0))))) → c65(0'(5(2(5(z0)))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(3(5(1(5(z0))))) → c67(0'(3(5(4(1(z0))))))
0'(4(2(1(5(z0))))) → c69(0'(2(5(4(4(1(z0)))))))
0'(4(2(1(5(z0))))) → c70(0'(4(1(5(3(2(z0)))))))
0'(4(2(1(5(z0))))) → c71(0'(0(5(z0))), 0'(5(z0)))
0'(4(2(1(5(z0))))) → c72(0'(5(z0)))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c74(0'(1(5(2(4(z0))))))
0'(4(2(1(5(z0))))) → c75(0'(5(2(4(1(z0))))))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(2(1(5(z0))))) → c77(0'(1(5(2(z0)))))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(4(2(0(2(z0))))) → c68(0'(0(4(3(2(2(z0)))))), 0'(4(3(2(2(z0))))))
0'(1(2(0(z0)))) → c22(0'(2(4(1(0(3(z0)))))), 0'(3(z0)))
0'(0(2(1(5(z0))))) → c29(0'(0(2(5(4(1(z0)))))), 0'(2(5(4(1(z0))))))
0'(1(0(4(5(z0))))) → c31(0'(4(0(0(1(5(z0)))))), 0'(0(1(5(z0)))), 0'(1(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(1(2(0(2(z0))))) → c44(0'(4(0(1(2(2(z0)))))), 0'(1(2(2(z0)))))
0'(1(4(5(0(z0))))) → c46(0'(5(4(1(0(3(z0)))))), 0'(3(z0)))
0'(2(0(1(5(z0))))) → c48(0'(0(2(3(5(z0))))), 0'(2(3(5(z0)))))
0'(2(0(4(5(z0))))) → c49(0'(0(2(4(1(5(z0)))))), 0'(2(4(1(5(z0))))))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))

S tuples:

0'(1(1(2(z0)))) → c(0'(1(3(2(z0)))))
0'(1(1(2(z0)))) → c1(0'(1(2(z0))))
0'(1(1(2(z0)))) → c2(0'(1(4(1(3(2(z0)))))))
0'(1(1(2(z0)))) → c3(0'(4(1(4(1(2(z0)))))))
0'(1(1(2(z0)))) → c4(0'(3(1(2(z0)))))
0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c8(0'(4(1(0(1(5(z0)))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c10(0'(1(3(1(5(z0))))))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c12(0'(1(5(4(1(z0))))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c16(0'(1(5(3(z0)))))
0'(1(1(5(z0)))) → c17(0'(1(5(4(z0)))))
0'(1(1(5(z0)))) → c18(0'(5(z0)))
0'(1(1(5(z0)))) → c19(0'(5(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(2(0(z0)))) → c22(0'(2(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(3(5(z0)))) → c23(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c24(0'(3(5(4(1(z0))))))
0'(1(4(5(z0)))) → c25(0'(1(5(3(z0)))))
0'(2(4(5(z0)))) → c26(0'(2(3(5(z0)))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(2(4(5(z0)))) → c28(0'(3(2(3(5(z0))))))
0'(0(2(1(5(z0))))) → c29(0'(0(2(5(4(1(z0)))))), 0'(2(5(4(1(z0))))))
0'(1(0(4(5(z0))))) → c31(0'(4(0(0(1(5(z0)))))), 0'(0(1(5(z0)))), 0'(1(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(1(1(3(5(z0))))) → c36(0'(1(3(5(z0)))))
0'(1(1(3(5(z0))))) → c37(0'(3(1(z0))))
0'(1(1(4(2(z0))))) → c38(0'(4(1(4(1(2(z0)))))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c41(0'(5(4(1(3(1(z0)))))))
0'(1(1(4(5(z0))))) → c42(0'(5(4(1(4(1(z0)))))))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(2(0(2(z0))))) → c44(0'(4(0(1(2(2(z0)))))), 0'(1(2(2(z0)))))
0'(1(2(1(5(z0))))) → c45(0'(1(4(1(2(5(z0)))))))
0'(1(4(5(0(z0))))) → c46(0'(5(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(0(1(5(z0))))) → c48(0'(0(2(3(5(z0))))), 0'(2(3(5(z0)))))
0'(2(0(4(5(z0))))) → c49(0'(0(2(4(1(5(z0)))))), 0'(2(4(1(5(z0))))))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))
0'(2(3(1(5(z0))))) → c51(0'(0(1(2(3(5(z0)))))), 0'(1(2(3(5(z0))))))
0'(2(3(1(5(z0))))) → c52(0'(2(5(3(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c53(0'(3(5(2(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c54(0'(4(1(3(5(z0))))))
0'(2(3(1(5(z0))))) → c55(0'(4(1(5(3(z0))))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c58(0'(5(2(3(z0)))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(3(1(5(z0))))) → c60(0'(3(z0)))
0'(2(5(1(2(z0))))) → c61(0'(2(3(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c62(0'(3(5(2(1(5(z0)))))))
0'(2(5(1(5(z0))))) → c63(0'(4(1(5(2(5(z0)))))))
0'(2(5(1(5(z0))))) → c64(0'(5(z0)))
0'(2(5(1(5(z0))))) → c65(0'(5(2(5(z0)))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(3(5(1(5(z0))))) → c67(0'(3(5(4(1(z0))))))
0'(4(2(0(2(z0))))) → c68(0'(0(4(3(2(2(z0)))))), 0'(4(3(2(2(z0))))))
0'(4(2(1(5(z0))))) → c69(0'(2(5(4(4(1(z0)))))))
0'(4(2(1(5(z0))))) → c70(0'(4(1(5(3(2(z0)))))))
0'(4(2(1(5(z0))))) → c71(0'(0(5(z0))), 0'(5(z0)))
0'(4(2(1(5(z0))))) → c72(0'(5(z0)))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c74(0'(1(5(2(4(z0))))))
0'(4(2(1(5(z0))))) → c75(0'(5(2(4(1(z0))))))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(2(1(5(z0))))) → c77(0'(1(5(2(z0)))))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c23, c24, c25, c26, c27, c28, c36, c37, c38, c39, c40, c41, c42, c43, c45, c47, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c69, c70, c71, c72, c73, c74, c75, c76, c77, c78, c68, c22, c29, c31, c32, c33, c34, c35, c44, c46, c48, c49, c50

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 49 of 78 dangling nodes:

0'(1(1(2(z0)))) → c(0'(1(3(2(z0)))))
0'(1(1(2(z0)))) → c1(0'(1(2(z0))))
0'(1(1(2(z0)))) → c2(0'(1(4(1(3(2(z0)))))))
0'(1(1(2(z0)))) → c3(0'(4(1(4(1(2(z0)))))))
0'(1(1(2(z0)))) → c4(0'(3(1(2(z0)))))
0'(1(1(5(z0)))) → c10(0'(1(3(1(5(z0))))))
0'(1(1(5(z0)))) → c12(0'(1(5(4(1(z0))))))
0'(1(1(5(z0)))) → c16(0'(1(5(3(z0)))))
0'(1(1(5(z0)))) → c18(0'(5(z0)))
0'(1(1(5(z0)))) → c17(0'(1(5(4(z0)))))
0'(1(1(5(z0)))) → c19(0'(5(z0)))
0'(1(2(0(z0)))) → c22(0'(2(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(4(5(z0)))) → c24(0'(3(5(4(1(z0))))))
0'(1(3(5(z0)))) → c23(0'(3(5(4(1(z0))))))
0'(2(4(5(z0)))) → c26(0'(2(3(5(z0)))))
0'(1(4(5(z0)))) → c25(0'(1(5(3(z0)))))
0'(2(4(5(z0)))) → c28(0'(3(2(3(5(z0))))))
0'(0(2(1(5(z0))))) → c29(0'(0(2(5(4(1(z0)))))), 0'(2(5(4(1(z0))))))
0'(1(1(3(5(z0))))) → c37(0'(3(1(z0))))
0'(1(1(4(2(z0))))) → c38(0'(4(1(4(1(2(z0)))))))
0'(1(1(3(5(z0))))) → c36(0'(1(3(5(z0)))))
0'(1(1(4(5(z0))))) → c41(0'(5(4(1(3(1(z0)))))))
0'(1(1(4(5(z0))))) → c42(0'(5(4(1(4(1(z0)))))))
0'(1(2(1(5(z0))))) → c45(0'(1(4(1(2(5(z0)))))))
0'(1(4(5(0(z0))))) → c46(0'(5(4(1(0(3(z0)))))), 0'(3(z0)))
0'(1(2(0(2(z0))))) → c44(0'(4(0(1(2(2(z0)))))), 0'(1(2(2(z0)))))
0'(2(0(4(5(z0))))) → c49(0'(0(2(4(1(5(z0)))))), 0'(2(4(1(5(z0))))))
0'(2(0(1(5(z0))))) → c48(0'(0(2(3(5(z0))))), 0'(2(3(5(z0)))))
0'(2(3(1(5(z0))))) → c54(0'(4(1(3(5(z0))))))
0'(2(3(1(5(z0))))) → c53(0'(3(5(2(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c52(0'(2(5(3(4(1(z0)))))))
0'(2(3(1(5(z0))))) → c51(0'(0(1(2(3(5(z0)))))), 0'(1(2(3(5(z0))))))
0'(2(3(1(5(z0))))) → c58(0'(5(2(3(z0)))))
0'(2(3(1(5(z0))))) → c55(0'(4(1(5(3(z0))))))
0'(2(5(1(5(z0))))) → c62(0'(3(5(2(1(5(z0)))))))
0'(2(5(1(2(z0))))) → c61(0'(2(3(2(1(5(z0)))))))
0'(2(3(1(5(z0))))) → c60(0'(3(z0)))
0'(3(5(1(5(z0))))) → c67(0'(3(5(4(1(z0))))))
0'(4(2(0(2(z0))))) → c68(0'(0(4(3(2(2(z0)))))), 0'(4(3(2(2(z0))))))
0'(4(2(1(5(z0))))) → c69(0'(2(5(4(4(1(z0)))))))
0'(4(2(1(5(z0))))) → c70(0'(4(1(5(3(2(z0)))))))
0'(2(5(1(5(z0))))) → c63(0'(4(1(5(2(5(z0)))))))
0'(2(5(1(5(z0))))) → c64(0'(5(z0)))
0'(2(5(1(5(z0))))) → c65(0'(5(2(5(z0)))))
0'(4(2(1(5(z0))))) → c75(0'(5(2(4(1(z0))))))
0'(4(2(1(5(z0))))) → c77(0'(1(5(2(z0)))))
0'(4(2(1(5(z0))))) → c71(0'(0(5(z0))), 0'(5(z0)))
0'(4(2(1(5(z0))))) → c72(0'(5(z0)))
0'(4(2(1(5(z0))))) → c74(0'(1(5(2(4(z0))))))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c8(0'(4(1(0(1(5(z0)))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(4(5(z0))))) → c31(0'(4(0(0(1(5(z0)))))), 0'(0(1(5(z0)))), 0'(1(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c8(0'(4(1(0(1(5(z0)))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(0(4(5(z0))))) → c31(0'(4(0(0(1(5(z0)))))), 0'(0(1(5(z0)))), 0'(1(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c8, c9, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c31, c32, c33, c34, c35, c50

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))
0'(1(1(5(z0)))) → c(0'(4(1(0(1(5(z0)))))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(4(0(0(1(5(z0)))))))
0'(1(0(4(5(z0))))) → c(0'(0(1(5(z0)))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c9(0'(5(4(1(0(1(z0)))))), 0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(4(1(2(1(0(z0)))))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(0(z0)), 0'(z0))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(0(5(0(z0))))) → c50(0'(2(5(0(3(0(z0)))))), 0'(3(0(z0))), 0'(z0))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(4(1(0(1(5(z0)))))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(4(0(0(1(5(z0)))))))
0'(1(0(4(5(z0))))) → c(0'(0(1(5(z0)))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c9, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c32, c33, c34, c35, c50, c

(9) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 9 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(5(z0)))) → c
0'(1(0(4(5(z0))))) → c

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(5(z0)))) → c
0'(1(0(4(5(z0))))) → c

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c33, c, c9, c32, c34, c35, c50, c

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace 0'(1(1(0(5(z0))))) → c33(0'(4(0(1(5(z0))))), 0'(1(5(z0)))) by

0'(1(1(0(5(1(5(z0))))))) → c33(0'(4(5(4(1(0(1(5(z0)))))))), 0'(1(5(1(5(z0))))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(5(z0)))) → c
0'(1(0(4(5(z0))))) → c
0'(1(1(0(5(1(5(z0))))))) → c33(0'(4(5(4(1(0(1(5(z0)))))))), 0'(1(5(1(5(z0))))))

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(5(z0)))) → c
0'(1(0(4(5(z0))))) → c
0'(1(1(0(5(1(5(z0))))))) → c33(0'(4(5(4(1(0(1(5(z0)))))))), 0'(1(5(1(5(z0))))))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c, c33

(13) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 2 of 31 dangling nodes:

0'(1(1(5(z0)))) → c
0'(1(0(4(5(z0))))) → c

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c33(0'(4(5(4(1(0(1(5(z0)))))))), 0'(1(5(1(5(z0))))))

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c33(0'(4(5(4(1(0(1(5(z0)))))))), 0'(1(5(1(5(z0))))))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c33

(15) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(4(5(4(1(0(1(5(z0)))))))))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(4(5(4(1(0(1(5(z0)))))))))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1

(17) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

K tuples:none
Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [1] + [2]x₁ + x₁²   
POL(0'(x₁)) = [2] + [2]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = x₁   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [1] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [2]x₁ + x₁²   
POL(0'(x₁)) = x₁   
POL(1(x₁)) = [1] + x₁   
POL(2(x₁)) = x₁   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [2] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(z0))

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [2]x₁²   
POL(0'(x₁)) = [3] + [2]x₁²   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [2] + x₁   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [2] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(z0))

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁ + x₁²   
POL(0'(x₁)) = [3] + [2]x₁²   
POL(1(x₁)) = [2] + x₁   
POL(2(x₁)) = x₁   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(2(0(5(0(z0))))) → c50(0'(z0))

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(27) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(2(0(5(0(z0))))) → c50(0'(z0))

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁ + x₁²   
POL(0'(x₁)) = [1] + x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = x₁   
POL(3(x₁)) = [1] + x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [1] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(2(0(5(0(z0))))) → c50(0'(z0))

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(1(4(2(z0))))) → c39(0'(z0))

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁ + x₁²   
POL(0'(x₁)) = [2]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [1] + x₁   
POL(3(x₁)) = [2] + x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [2] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(4(2(z0))))) → c39(0'(z0))

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(1(1(4(2(z0))))) → c40(0'(1(z0)))

We considered the (Usable) Rules:

0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))

And the Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁ + x₁²   
POL(0'(x₁)) = [3] + x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [1] + x₁   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [2] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c21(x₁)) = x₁   
POL(c27(x₁)) = x₁   
POL(c32(x₁, x₂)) = x₁ + x₂   
POL(c34(x₁)) = x₁   
POL(c35(x₁)) = x₁   
POL(c39(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c43(x₁)) = x₁   
POL(c47(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c50(x₁)) = x₁   
POL(c56(x₁)) = x₁   
POL(c57(x₁)) = x₁   
POL(c59(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c66(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c73(x₁)) = x₁   
POL(c76(x₁)) = x₁   
POL(c78(x₁)) = x₁   
POL(c9(x₁)) = x₁   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(2(z0)))) → 1(0(1(3(2(z0)))))
0(1(1(2(z0)))) → 4(1(0(1(2(z0)))))
0(1(1(2(z0)))) → 0(1(4(1(3(2(z0))))))
0(1(1(2(z0)))) → 0(4(1(4(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(0(3(1(2(z0))))))
0(1(1(2(z0)))) → 4(1(3(1(0(2(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(z0)))))
0(1(1(5(z0)))) → 5(4(1(0(1(z0)))))
0(1(1(5(z0)))) → 0(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 0(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 1(0(1(3(1(5(z0))))))
0(1(1(5(z0)))) → 1(4(4(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(0(1(5(4(1(z0))))))
0(1(1(5(z0)))) → 3(4(1(0(1(5(z0))))))
0(1(1(5(z0)))) → 3(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 3(5(4(1(0(1(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(3(z0))))))
0(1(1(5(z0)))) → 4(1(0(1(5(4(z0))))))
0(1(1(5(z0)))) → 4(1(3(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(1(4(1(0(5(z0))))))
0(1(1(5(z0)))) → 4(4(1(5(0(1(z0))))))
0(1(1(5(z0)))) → 5(4(1(3(1(0(z0))))))
0(1(2(0(z0)))) → 0(2(4(1(0(3(z0))))))
0(1(3(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 0(3(5(4(1(z0)))))
0(1(4(5(z0)))) → 4(4(0(1(5(3(z0))))))
0(2(4(5(z0)))) → 4(0(2(3(5(z0)))))
0(2(4(5(z0)))) → 4(4(0(2(5(z0)))))
0(2(4(5(z0)))) → 4(0(3(2(3(5(z0))))))
0(0(2(1(5(z0))))) → 0(0(2(5(4(1(z0))))))
0(0(2(4(5(z0))))) → 0(0(4(4(2(5(z0))))))
0(1(0(4(5(z0))))) → 0(4(0(0(1(5(z0))))))
0(1(0(5(0(z0))))) → 4(1(5(0(0(0(z0))))))
0(1(1(0(5(z0))))) → 1(0(4(0(1(5(z0))))))
0(1(1(2(0(z0))))) → 0(4(1(2(1(0(z0))))))
0(1(1(2(0(z0))))) → 4(1(2(1(0(0(z0))))))
0(1(1(3(5(z0))))) → 4(1(0(1(3(5(z0))))))
0(1(1(3(5(z0))))) → 5(4(1(0(3(1(z0))))))
0(1(1(4(2(z0))))) → 0(4(1(4(1(2(z0))))))
0(1(1(4(2(z0))))) → 4(1(3(1(2(0(z0))))))
0(1(1(4(2(z0))))) → 4(2(4(1(0(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(4(5(z0))))) → 0(5(4(1(4(1(z0))))))
0(1(1(4(5(z0))))) → 2(4(1(0(1(5(z0))))))
0(1(2(0(2(z0))))) → 0(4(0(1(2(2(z0))))))
0(1(2(1(5(z0))))) → 0(1(4(1(2(5(z0))))))
0(1(4(5(0(z0))))) → 0(5(4(1(0(3(z0))))))
0(1(5(1(5(z0))))) → 5(4(1(0(1(5(z0))))))
0(2(0(1(5(z0))))) → 1(0(0(2(3(5(z0))))))
0(2(0(4(5(z0))))) → 0(0(2(4(1(5(z0))))))
0(2(0(5(0(z0))))) → 0(2(5(0(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(0(1(2(3(5(z0))))))
0(2(3(1(5(z0))))) → 0(2(5(3(4(1(z0))))))
0(2(3(1(5(z0))))) → 0(3(5(2(4(1(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(3(5(z0))))))
0(2(3(1(5(z0))))) → 2(0(4(1(5(3(z0))))))
0(2(3(1(5(z0))))) → 2(3(5(3(0(1(z0))))))
0(2(3(1(5(z0))))) → 2(5(3(4(1(0(z0))))))
0(2(3(1(5(z0))))) → 4(1(0(5(2(3(z0))))))
0(2(3(1(5(z0))))) → 4(1(3(0(2(5(z0))))))
0(2(3(1(5(z0))))) → 4(1(5(2(0(3(z0))))))
0(2(5(1(2(z0))))) → 0(2(3(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(3(5(2(1(5(z0))))))
0(2(5(1(5(z0))))) → 0(4(1(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 2(4(1(5(0(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(0(5(2(5(z0))))))
0(2(5(1(5(z0))))) → 4(1(5(5(2(0(z0))))))
0(3(5(1(5(z0))))) → 5(0(3(5(4(1(z0))))))
0(4(2(0(2(z0))))) → 0(0(4(3(2(2(z0))))))
0(4(2(1(5(z0))))) → 0(2(5(4(4(1(z0))))))
0(4(2(1(5(z0))))) → 0(4(1(5(3(2(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(0(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(3(0(5(z0))))))
0(4(2(1(5(z0))))) → 2(4(1(5(4(0(z0))))))
0(4(2(1(5(z0))))) → 3(0(1(5(2(4(z0))))))
0(4(2(1(5(z0))))) → 3(0(5(2(4(1(z0))))))
0(4(2(1(5(z0))))) → 4(1(3(2(5(0(z0))))))
0(4(2(1(5(z0))))) → 4(4(0(1(5(2(z0))))))
0(4(5(1(5(z0))))) → 5(4(1(5(0(4(z0))))))

Tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(1(0(5(1(5(z0))))))) → c1

S tuples:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))

K tuples:

0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(4(2(1(5(z0))))) → c73(0'(z0))
0'(1(1(5(z0)))) → c6(0'(1(5(z0))))
0'(1(1(5(z0)))) → c7(0'(1(z0)))
0'(1(1(5(z0)))) → c11(0'(1(5(z0))))
0'(1(1(5(z0)))) → c14(0'(1(z0)))
0'(1(1(5(z0)))) → c20(0'(1(z0)))
0'(1(1(4(5(z0))))) → c43(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(4(2(1(5(z0))))) → c76(0'(z0))
0'(4(5(1(5(z0))))) → c78(0'(4(z0)))
0'(1(0(5(0(z0))))) → c32(0'(0(0(z0))), 0'(z0))
0'(1(1(2(0(z0))))) → c35(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1
0'(1(1(5(z0)))) → c15(0'(1(z0)))
0'(1(1(5(z0)))) → c21(0'(z0))
0'(1(0(4(5(z0))))) → c(0'(1(5(z0))))
0'(1(1(2(0(z0))))) → c34(0'(z0))
0'(1(1(0(5(1(5(z0))))))) → c1(0'(1(5(1(5(z0))))))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(1(1(5(z0)))) → c9(0'(1(z0)))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(1(4(2(z0))))) → c39(0'(z0))
0'(1(1(4(2(z0))))) → c40(0'(1(z0)))

Defined Rule Symbols:

0

Defined Pair Symbols:

0'

Compound Symbols:

c5, c6, c7, c11, c13, c14, c15, c20, c21, c27, c39, c40, c43, c47, c56, c57, c59, c66, c73, c76, c78, c, c9, c32, c34, c35, c50, c1, c1

(33) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

0'(1(1(2(z0)))) → c5(0'(2(z0)))
0'(1(1(5(z0)))) → c13(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(1(1(5(z0)))) → c(0'(1(5(z0))))
0'(2(4(5(z0)))) → c27(0'(2(5(z0))))
0'(2(3(1(5(z0))))) → c56(0'(1(z0)))
0'(2(3(1(5(z0))))) → c57(0'(z0))
0'(2(3(1(5(z0))))) → c59(0'(2(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(2(0(5(0(z0))))) → c50(0'(z0))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))
0'(2(5(1(5(z0))))) → c66(0'(z0))
0'(1(5(1(5(z0))))) → c47(0'(1(5(z0))))

Now S is empty

(34) BOUNDS(O(1), O(1))